 $LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
 require 'ext_pr1_v4'

#Datendefinitionen:
#
#1D Objekte
#
#Point1d ::= Int
 
def_class(:Point1d,[:int]) {
  def invariant?() 
    int.int?
  end
}

#Range1d ::= Range[first,last] :: Point1d x Point1d

def_class(:Range1d,[:first,:last]){
  def invariant?()
    first.point1d?
    last.point1d?
  end
}
#SINN?
def range1d(o)
  check_pre((o.first.point1d? and o.last.point1d?))
  
end

#Union1d ::= Union1d[left,right] :: Shape1d x Shape1d

def_class(:Union1d, [:left, :right]) {
  def invariant?()
    shape1d?(left)
    shape1d?(right)
  end
}

#Shape1d ::= Range1d | Union1d

def shape1d?(value)
  value.range1d? or value.union1d?
end

#2D Objekte
#
#Point2d :: = Point2d[x,y] :: Point1d x Point1d

def_class(:Point2d, [:x, :y]){
 def invariant?()
   x.point1d?
   y.point1d?
 end
}

#Range2d ::= Range2d[x_range,y_range] :: (Range1d x Range1d)

def_class(:Range2d, [:x_range, :y_range]){
 def invariant?()
   x_range.range1d?
   y_range.range1d?
 end
}

#Union2d ::= Union2d[left,right] :: Shape2d x Shape2d

def_class(:Union2d, [:left, :right]){
 def invariant?()
   shape2d?(left)
   shape2d?(right)
 end
}

#Shape2d ::= Range2d | Union2d

def shape2d?(value)
  value.range2d? or value.union2d?
end

#Point ::= Point1d | Point2d

def point?(value)
  value.point1d? or value.point2d?
end

#PrimShape ::= Range1d | Range2d

def prim_shape?(value)
    value.range1d? or value.range2d?
end

#UnionShape ::= Union1d | Union2d

def union_shape?(value)
  value.union1d? or value.union2d?
end

#CompShape ::= UnionShape

def comp_shape?(value)
  union_shape?(value)
end

#Shape ::= PrimShape | CompShape

def shape?(value)
  prim_shape?(value) or comp_shape?(value)
end

#GraphObj ::= Point | Shape

def graph_obj(value)
  point?(value) or value.shape?
end

#translate ::= (shape, point) :: Shape x Point ->? Shape

def translate(shape, point)
  if (shape1d?(shape) and point.point1d?) then
    trans1d(shape, point)
  elsif (shape2d?(shape) and point.point2d?) then
    trans2d(shape, point)
  elsif (point1d?(shape) and point.point1d?) then
    trans0d
  else
    check_pre((false))
  end
end

#trans0d ::= (point1, point2) :: Point1d x Point1d -> Point1d

def trans0d(point1, point2)  
  Point1d[point1.int + point2.int]
end

#trans1d ::= (shape1d, point1d) :: Shape1d x Point1d ->? Shape1d

def trans1d(shape1d, point1d)
  check_pre((shape1d?(shape1d) and point1d.point1d?))
  if (shape1d.range1d?) then
    Range1d[trans0d(shape1d.first, point1d), trans0d(shape1d.last, point1d)]
  elsif shape1d.union1d? then
    Union1d[trans1d(shape1d.left, point1d), trans1d(shape1d.right, point1d)]
  else
    check_pre((false))
  end
end

#trans2d ::= (shape2d, point2d) :: Shape2d x Point2d ->? Shape2d

def trans2d(shape2d, point2d)
  check_pre((shape2d?(shape2d) and point2d.point2d?))
  if (shape2d.range2d?) then
    Range2d[trans1d(shape2d.x_range, point2d.x), trans1d(shape2d.y_range, point2d.y)]
  elsif shape2d.union2d? then
    Union2d[trans2d(shape2d.left, point2d), trans2d(shape2d.right, point2d)]  
  else
    check_pre((false))
  end 
end

#bounding_range ::= (r1,r2) :: (Range1d x Range1d) -> Range1d | (Range2d x Range2d) -> Range2d

def bounding_range(r1,r2)
    if (r1.range1d? and r2.range1d?) then
      first = find_min(r1.first.int, r2.first.int)
      last = find_max(r1.last.int, r2.last.int)
      Range1d[Point1d[first],Point1d[last]]
    elsif 
      (r1.range2d? and r2.range2d?) then
      x_first = find_min(r1.x_range.first.int, r2.x_range.first.int)
      x_last = find_max(r1.x_range.last.int, r2.x_range.last.int)
      x_range_new = Range1d[Point1d[x_first], Point1d[x_last]]
      y_first = find_min(r1.y_range.first.int, r2.y_range.first.int)
      y_last = find_max(r1.y_range.last.int, r2.y_range.last.int)
      y_range_new = Range1d[Point1d[y_first], Point1d[y_last]]
      Range2d[x_range_new, y_range_new]
    else
      check_pre((false))
    end
end

def find_min(r1, r2) r1 < r2 ? r1 : r2 end

def find_max(r1, r2) r1 < r2 ? r2 : r1 end

#bounds ::= (shape) :: Shape -> (Range1d | Range2d)

def bounds(shape)
  if (union_shape?(shape)) then
    if (not union_shape?(shape.left) and not union_shape?(shape.right)) then
      bounding_range(shape.left, shape.right)
    else
      bounds(shape.left)
      bounds(shape.right)
    end
  else
    bounding_range(shape.left, shape.right)
  end
end

#Äquivalenzprädikate (Gleichheiten)
#
#VERSION 1:
#
#graph_equal_? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#

def graph_equal_v1_?(o1, o2)
  check_pre((graph_obj(o1) and graph_obj(o2)))
  graph_equal_?(o1, o2)
end

def get_range(val1)
  if (union_shape?(val1)) then
    get_range(val1.left)
    get_range(val1.right)
  end
end

#
#VERSION 2:
#
#graph_equal? ::= (o1,o2) :: Any x Any ->? Bool

#def graph_equal_?(o1, o2)
#  check_pre((graph_obj(o1) and graph_obj(o2)))
#    
#end

def graph_equal_?(o1, o2)
   check_pre((graph_obj(o1) and graph_obj(o2)))
   if (o1.point1d? and o2.point1d?) or
      (o1.point2d? and o2.point2d?) or 
      (shape1d?(o1) and shape1d?(o2)) or
      (shape2d?(o1) and shape2d?(o2)) then
      o1 == o2
   else
    check_pre((false))
   end
end

#graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool

def graph_equal_trans?(o1, o2)
  check_pre(((point?(o1) and point?(o2)) or (shape?(o1) and shape?(o2))))
  # Punkte sind immer Deckungsgleich!!!
  if (o1.point1d? and o2.point1d?) or (o1.point2d? and o2.point2d?) then
    puts(o1)
    puts(o2)
    o1 == o2
  elsif (shape1d?(o1) and shape1d?(o2)) then
      if (o1.range1d? and o2.range1d?) then
        ((o1.last.int) - (o1.first.int)) == ((o2.last.int) - (o2.first.int))
      else
        graph_equal_trans?(bounds(o1), bounds(o2))
      end
  elsif (shape2d?(o1) and shape2d?(o2)) then
      if (o1.range2d? and o2.range2d?) then
        ((o1.x_range.first.int) - (o1.x_range.last.int)) == ((o2.x_range.first.int) - (o2.x_range.last.int)) and
        ((o1.y_range.first.int) - (o1.y_range.last.int)) == ((o2.y_range.first.int) - (o2.y_range.last.int))        
      else
        graph_equal_trans?(bounds(o1), bounds(o2))
      end
  else
    check_pre((false))
  end
end

#in? ::= (point, shape) :: Point x Shape -> Bool
def in?(val1, val2)
  check_pre((point?(val1) and shape?(val2)))
 if (val1.point1d? and shape1d?(val2)) then
   val1.int.between?(val2.first.int, val2.last.int)
 elsif (val1.point2d? and shape2d?(val2)) then
   (val1.x.int < val2.x_range.first.int or 
    val1.x.int > val2.x_range.last.int  or 
    val1.y.int < val2.y_range.first.int  or 
    val1.y.int > val2.y_range.last.int)
 elsif (val1.point1d? and val2.union1d?) or (val1.point2d? and val2.union2d?) then
   in?(val1,val2)
 end
end